Assigned Reading
Table of Contents
For next week (20 July 2022) you should read both of the following:
- The article You Could Have Invented Monads!, available by clicking here.
- My post about equational reasoning and
State, below. This is an expanded version of my answer to Question 425 on the course forum.
1 Equational Reasoning and State
In Lecture 5, we defined our own version of the State s monad, using the following
type declaration:
type State s a = s -> (s, a)
Keep in mind that the standard libraries define State in a slightly different way!
We also defined two functions for working with State s, bindS and yield, defined as follows:
bindS :: State s a -> (a -> State s b) -> State s b bindS f rest = \origState -> let (newState, retVal) = f origState in rest retVal newState -- yield returns its argument, and leaves the state unchanged yield :: a -> State s a yield v = \origState -> (origState, v) -- get returns the current state without changing it get :: State s s get = \origState -> (origState, origState) -- put replaces the state with the given argument (i.e. updates the state) put :: s -> State s () put newState = \origState -> (newState, ())
Recall that we used these operations (which, we now know, correspond to the monadic >>= and return) to implement
the label and label' functions, which do exactly the same thing. The latter uses State, the former does not,
but they implement exactly the same function.
But as far as functions go, even label itself is quite complicated. To really understand how State~/~bindS work
and what they buy us, we have to start with a much simpler function. In this worked example, our goal is to understand
the use function, which had two different implementations in the lecture.
One of these implementations is very simple and straightforward, while the other relies on bindS, get and put.
use :: State Integer Integer use = \lun -> (lun + 1, lun) use' :: State Integer Integer use' = bindS get $ \lun -> bindS (put (lun + 1)) $ \() -> yield lun
Again, these two implement exactly the same function. You can try this by calling them on the repl:
you'll see that e.g. use 5 and use' 5 both return the pair (6,5). Both of them are functions
of type Integer -> (Integer, Integer). What bindS gives us is a generally better, more convenient
way of implementing functions of the type s -> (s, a). But how does it work?
Well, the great thing about Haskell is that equational reasoning is always valid.
This means that, in principle, you can wrap your head around bindS by expanding out its definition,
using equational reasoning. This is the derivation we'll do below. Now, it won't be easy:
to follow along with the derivation, you should have a Haskell repl open, and test that use'
still type-checks, compiles and has same output after every change that we make.
In the end, once you understand what's happening, you should attempt to re-do this derivation completely by yourself, without referring to my write-up.
2 The derivation
We will start out with the definition of use'' below, and refactor it step-by-step via equational
reasoning. Our goal is to get rid of all the State-specific stuff, the bindS, get, put and yield
functions, and arrive to something that looks like the definition of use. This will prove that the
two functions do exactly the same thing.
use'' :: State Integer Integer use'' = bindS get $ \lun -> bindS (put (lun + 1)) $ \() -> yield lun
2.1 Step 1
Since bindS get $ \lun -> ... just means the same thing as bindS get (\lun -> ...),
we can factor out that second argument into a separate function using a where clause.
use'' :: State Integer Integer use'' = bindS get restOfUse where restOfUse = \lun -> bindS (put (lun + 1)) $ \() -> yield lun
2.2 Step 2
From here on, we'll be simplifying the part outside of the where block. The goal is to get rid of bindS from there. This can be done via some equational reasoning: I will take the definition of bindS f rest = ..., given above, and replace bindS get restOfUse with the right hand side of that definition. Here's what we get:
use'' :: State Integer Integer use'' = \origState -> let (newState, retVal) = get origState in restOfUse retVal newState where restOfUse = \lun -> bindS (put (lun + 1)) $ \() -> yield lun
2.3 Step 3
We got rid of bindS (outside the where block), but another State-related function, get, is still there. We can rid ourselves of the get function too, by using equational reasoning again. The definiton given above is the same as get x = (x,x).
use'' :: State Integer Integer use'' = \origState -> let (newState, retVal) = (origState, origState) in restOfUse retVal newState where restOfUse = \lun -> bindS (put (lun + 1)) $ \() -> yield lun
2.4 Step 4
We will now rename the origState argument to w. We're allowed to do this, of course: the names of function arguments don't matter. Why do we do this? Well, on one hand shorter names are easier to read. On the other hand, it will avoid a name clash much later (you'll see where, but there's no need to worry about it for now).
use'' :: State Integer Integer use'' = \w -> let (newState, retVal) = (w, w) in restOfUse retVal newState where restOfUse = \lun -> bindS (put (lun + 1)) $ \() -> yield lun
2.5 Step 5
We can now get rid of that annoying let binding, simply by substituting the variables newState and retVal with w.
use'' :: State Integer Integer use'' = \w -> restOfUse w w where restOfUse = \lun -> bindS (put (lun + 1)) $ \() -> yield lun
2.6 Step 6
The part outside the where clause is fairly simple now: we don't see how one could simplify it further. So, let's switch our attention to the restOfUse function inside the where clause. How could we simplify that? Before we simplify it, I'll replace restOfUse = \lun -> ... with restOfUse lun = ... just to make things slightly easier to read.
use'' :: State Integer Integer use'' = \w -> restOfUse w w where restOfUse lun = bindS (put (lun + 1)) $ \() -> yield lun
2.7 Step 7
Now, we'll do the same thing we did in the first step: replace bindS f $ ... with bindS f (...) to make it clear what the two arguments actually are.
use'' :: State Integer Integer use'' = \w -> restOfUse w w where restOfUse lun = bindS (put (lun + 1)) (\() -> yield lun)
2.8 Step 8
Time to get rid of the bindS via equational reasoning! Again, just use the right-hand side of the definition given in the lecture (or above, refer back to the code!)
use'' :: State Integer Integer use'' = \w -> restOfUse w w where restOfUse lun = \origState -> let (newState, retVal) = put (lun + 1) origState in (\() -> yield lun) retVal newState
2.9 Step 9
We got rid of bindS, but we still have other state-specific functions, e.g. put. We get rid
of put using some more equational reasoning, by using the definition put y x = (y, ()) (You should of course convince yourself that this is the same definition as the one given in the lecture!)
use'' :: State Integer Integer use'' = \w -> restOfUse w w where restOfUse lun = \origState -> let (newState, retVal) = (lun + 1, ()) in (\() -> yield lun) retVal newState
2.10 Step 10
As before, we can get rid of a let binding by substituting newState with lun + 1 and retVal with ().
use'' :: State Integer Integer use'' = \w -> restOfUse w w where restOfUse lun = \origState -> (\() -> yield lun) () (lun + 1)
2.11 Step 11
Let's get rid of that weird-looking (\() ->) function application too. What does it mean anyway?
Well, () is a type, with one constructor, confusingly also denoted (). So what is \() -> yield lun? It's a function that takes an argument of type (), pattern matches it against the value () (which will always succeed since the only value of type () is the value ()) and then returns yield lun. We could have written \_ -> yield lun or \q -> yield lun, these functions all do the same thing.
Now, what happens when you evaluate (\() -> yield lun) ()? Well, you're just applying the function \() -> yield lun to the value (). So it will return yield lun. Here's what we get:
use'' :: State Integer Integer use'' = \w -> restOfUse w w where restOfUse lun = \origState -> yield lun (lun + 1)
2.12 Step 12
Our last bit of equational reasoning: we use the definition yield v x = (x, v) (as usual, convince yourself that this is the same as the one given above!)
use'' :: State Integer Integer use'' = \w -> restOfUse w w where restOfUse lun = \origState -> (lun + 1, lun)
2.13 Step 13
It should be clear where this is going now. Let's just get rid of the \origState -> lambda.
use'' :: State Integer Integer use'' = \w -> restOfUse w w where restOfUse lun origState = (lun + 1, lun)
2.14 Step 14
Remember, we only introduced restOfUse to make things easier to read! Now it's no longer useful, so we can get rid of it, along with the whole where block. How? We can just replace restOfUse w w by the right hand side of the definition of restOfUse, which is (w + 1, w).
use'' :: State Integer Integer use'' = \w -> (w + 1, w)
And there we have it! We can now see that use'' and use are clearly the same function!
2.15 What did we learn?
We learned that there is no magic inside bindS, it really is just another way of writing ordinary functions of the form s -> (s,a). We can think of such functions as functions that manipulate a piece of state of type s, and ultimately return something of type a.
Previously (think back to label in Lecture 5) we had to write these functions by maintaining that piece of state manually, using a repetitive let (newState, rv) = ... syntax. But Haskell was powerful enough to let us capture this repetitive activity in a function, bindS. Thanks to bindS, we no longer have to explicitly deal with "threading" this state through our application. The code is easier to write, easier to read (for those readers who wrapped their heads around State), and we even eliminated a class of potential bugs (where we give the wrong state argument).
Of course, it's silly to use all this machinery for a trivially simple function like use , but the payoff is already substantial for slightly more complicated functions, such as label' vs label of Lecture 5.